{-@ LIQUID "--expect-any-error" @-}
module Inst00 where


-- | Typing classes
-- | Step 1: Refine type dictionaries:

class Compare a where
    cmax :: a -> a -> a
    cmin :: a -> a -> a

instance Compare Int where
{-@ instance Compare Int where
      cmax :: Odd -> Odd -> Odd ;
      cmin :: Int -> Int -> Int
  @-}

    cmax y x = if x >= y then x else y
    cmin y x = if x >= y then x else y

-- | creates dictionary environment:
-- | * add the following environment
-- | dictionary $fCompareInt :: Compare Int
-- |               { $ccmax :: Odd -> Odd -> Odd
-- |               , $ccmin :: Int -> Int -> Int
-- |               }
-- |
-- | Important: do not type dictionaries, as preconditions
-- | of fields cannot be satisfied!!!!!


-- | Dictionary application
-- | ((cmax Int)    @fcompareInt) :: Odd -> Odd -> Odd
-- | ((cmin Int)    @fcompareInt) :: Int -> Int -> Int
-- | (anything_else @fcompareInt) :: default


{-@ foo :: Odd -> Odd -> Odd @-}
foo :: Int -> Int -> Int
foo x y = cmax x y

{-@ unsafe :: Odd -> Odd -> Odd @-}
unsafe :: Int -> Int -> Int
unsafe x y = cmin x y
